\begin{tabbing} (\=(BLemma `list\_extensionality`) \+ \\[0ex]CollapseTHEN (Auto$\cdot$))$\cdot$ \- \end{tabbing}